f3(true, x, y) -> f3(gt2(x, y), trunc1(x), s1(y))
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
f3(true, x, y) -> f3(gt2(x, y), trunc1(x), s1(y))
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
TRUNC1(s1(s1(x))) -> TRUNC1(x)
F3(true, x, y) -> GT2(x, y)
F3(true, x, y) -> F3(gt2(x, y), trunc1(x), s1(y))
GT2(s1(u), s1(v)) -> GT2(u, v)
F3(true, x, y) -> TRUNC1(x)
f3(true, x, y) -> f3(gt2(x, y), trunc1(x), s1(y))
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TRUNC1(s1(s1(x))) -> TRUNC1(x)
F3(true, x, y) -> GT2(x, y)
F3(true, x, y) -> F3(gt2(x, y), trunc1(x), s1(y))
GT2(s1(u), s1(v)) -> GT2(u, v)
F3(true, x, y) -> TRUNC1(x)
f3(true, x, y) -> f3(gt2(x, y), trunc1(x), s1(y))
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
f3(true, x, y) -> f3(gt2(x, y), trunc1(x), s1(y))
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
TRUNC1(s1(s1(x))) -> TRUNC1(x)
f3(true, x, y) -> f3(gt2(x, y), trunc1(x), s1(y))
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
TRUNC1(s1(s1(x))) -> TRUNC1(x)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
TRUNC1(s1(s1(x))) -> TRUNC1(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), trunc1(x), s1(y))
f3(true, x, y) -> f3(gt2(x, y), trunc1(x), s1(y))
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), trunc1(x), s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
f3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), trunc1(x), s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), trunc1(s1(x0)), s1(s1(x1)))
F3(true, s1(x0), 0) -> F3(true, trunc1(s1(x0)), s1(0))
F3(true, 0, x0) -> F3(false, trunc1(0), s1(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
F3(true, s1(x0), 0) -> F3(true, trunc1(s1(x0)), s1(0))
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), trunc1(s1(x0)), s1(s1(x1)))
F3(true, 0, x0) -> F3(false, trunc1(0), s1(x0))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), trunc1(s1(x0)), s1(s1(x1)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)
F3(true, s1(0), s1(y1)) -> F3(gt2(0, y1), 0, s1(s1(y1)))
F3(true, s1(s1(x0)), s1(y1)) -> F3(gt2(s1(x0), y1), s1(s1(trunc1(x0))), s1(s1(y1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
F3(true, s1(0), s1(y1)) -> F3(gt2(0, y1), 0, s1(s1(y1)))
F3(true, s1(s1(x0)), s1(y1)) -> F3(gt2(s1(x0), y1), s1(s1(trunc1(x0))), s1(s1(y1)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
F3(true, s1(s1(x0)), s1(y1)) -> F3(gt2(s1(x0), y1), s1(s1(trunc1(x0))), s1(s1(y1)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)
F3(true, s1(s1(y_1)), s1(s1(z1))) -> F3(gt2(s1(y_1), s1(z1)), s1(s1(trunc1(y_1))), s1(s1(s1(z1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ UsableRulesProof
F3(true, s1(s1(y_1)), s1(s1(z1))) -> F3(gt2(s1(y_1), s1(z1)), s1(s1(trunc1(y_1))), s1(s1(s1(z1))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)
F3(true, s1(s1(y_1)), s1(s1(z1))) -> F3(gt2(y_1, z1), s1(s1(trunc1(y_1))), s1(s1(s1(z1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
F3(true, s1(s1(y_1)), s1(s1(z1))) -> F3(gt2(y_1, z1), s1(s1(trunc1(y_1))), s1(s1(s1(z1))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
F3(true, x, y) -> F3(gt2(x, y), trunc1(x), s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
f3(true, x0, x1)
gt2(s1(x0), 0)
f3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
F3(true, x, y) -> F3(gt2(x, y), trunc1(x), s1(y))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
trunc1(0) -> 0
trunc1(s1(0)) -> 0
trunc1(s1(s1(x))) -> s1(s1(trunc1(x)))
gt2(0, x0)
trunc1(s1(s1(x0)))
gt2(s1(x0), s1(x1))
trunc1(0)
trunc1(s1(0))
gt2(s1(x0), 0)